VERS5 
NIL 
((LISTINDUCTION LISPAX#30) (LISTINDUCTIONDEF LISPAX#34) (SEXPINDUCTION LISPAX#35) (SEXPINDUCTIONDEF LISPAX#36) (HIGH_ORDER_DEFINITION LISPAX#40) (LISTDEF LISPAX#45) (APPENDEF LISPAX#47) (LISTAPPEND LISPAX#48) (ALLPDEF LISPAX#52) (SOMEPDEF LISPAX#53) (MAPCARDEF LISPAX#54) (ALISTDEF1 LISPAX#57) (ALISTDEF LISPAX#58) (ASSOCDEF LISPAX#60) (MEMBERDEF LISPAX#63) (UNIQUENESSDEF LISPAX#65) (ALLPFACT ALLP#1) (ALLP_INTRODUCTION ALLP#2) (ALLP_ELIMINATION ALLP#3) (ALLP_IMPLICATION ALLP#4) (SOMEPFACT ALLP#5) (EPSILONDEF SETS#6) (SET_EXTENSIONALITY SETS#7) (INTERDEF SETS#9) (UNIONDEF SETS#11) (INCLUSIONDEF SETS#13) (MKSET_DEF SETS#17) (MKLSETDEF SETS#19) (MKSET_MKLSET SETFACTS#1) (DOUBLE_INCLUSION SETFACTS#2) (CONS_CAR_CDR LISPAX#28 LISPAX#29) (SIMPINFO LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4)) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (XV YV ZV) (TYPE: (TY& . GROUND)) (SORT: (TM& . URELEMENT))) . ((ZV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (YV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (XV . (GROUND . (SYMBOL& URELEMENT NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (URELEMENT . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (AV BV) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((BV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (AV . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|CAR NIL=NIL| . (AXIOM (TM& . |CAR NIL=NIL|)) . (CAR) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|CDR NIL=NIL| . (AXIOM (TM& . |CDR NIL=NIL|)) . (CDR) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#29) . NIL . LISPAX . NIL . 29 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30) . NIL . LISPAX . NIL . 30 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 32 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 33 .)(|∀X.URELEMENT(X)| . (AXIOM (TM& . |∀X.URELEMENT(X)|)) . (SEXP Z Y X URELEMENT ZV YV XV) . NIL . (SETS#3) . NIL . SETS . NIL . 3 .)(|∀XV.SEXP XV| . (AXIOM (TM& . |∀XV.SEXP XV|)) . (SEXP URELEMENT ZV YV XV) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(NIL . (DECL EPSILON (TYPE: (TY& . |(GROUND⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#5 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 5 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#35) . NIL . LISPAX . NIL . 35 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .))) . NIL . (LISPAX#36) . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#38 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 38 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS ARB BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#40) . NIL . LISPAX . NIL . 40 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#41 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 41 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#42 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 42 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#44) . NIL . LISPAX . NIL . 44 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#46 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 46 .)(|∀X U V.NIL*V=V∧X.U*V=X.(U*V)| . (DEFAX APPEND (TM& . |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#47 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀U V.LISTP U*V| . (AXIOM (TM& . |∀U V.LISTP U*V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(|∀U.U*NIL=U| . (AXIOM (TM& . |∀U.U*NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#49) . NIL . LISPAX . NIL . 49 .)(|∀X V.X.NIL*V=X.V| . (AXIOM (TM& . |∀X V.X.NIL*V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 51 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#51)) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#53 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#53) . NIL . LISPAX . NIL . 53 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . VARIABLE .))) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#55 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 55 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(|∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)| . (AXIOM (TM& . |∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)|)) . (CAR CDR ATOM NULL LISTP ALISTP W V U) . NIL . (LISPAX#57) . NIL . LISPAX . NIL . 57 .)(|∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#59 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 59 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#60) . NIL . LISPAX . NIL . 60 .)(|∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)| . (AXIOM (TM& . |∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP) . NIL . (ALLP#1) . NIL . ALLP . NIL . 1 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#62 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 62 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#63 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#63) . NIL . LISPAX . NIL . 63 .)(NIL . (DECL UNIQUENESS (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#64 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 64 .)(|∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))| . (DEFAX UNIQUENESS (TM& . |∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))|)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#65 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS MEMBER) . NIL . (LISPAX#65) . NIL . LISPAX . NIL . 65 .)(|∀U.SEXP CAR U| . (UE (UELST& (PHI . |λU.SEXP CAR U|)) (LN& . LISPAX#30) NIL) . (CAR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61) . NIL . LISPAX . NIL . 66 .)(|∀PHI1 U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)| . (AXIOM (TM& . |∀PHI1 U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP MEMBER (PHI1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . ALLP#2 . NIL . VARIABLE .))) . NIL . (ALLP#2) . NIL . ALLP . NIL . 2 .)(|∀U.LISTP CDR U| . (UE (UELST& (PHI . |λU.LISTP CDR U|)) (LN& . LISPAX#30) NIL) . (CDR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66) . NIL . LISPAX . NIL . 67 .)(|∀PHI1 X U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)| . (AXIOM (TM& . |∀PHI1 X U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP MEMBER PHI1) . NIL . (ALLP#3) . NIL . ALLP . NIL . 3 .)(|∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)| . (AXIOM (TM& . |∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)|)) . (LISTP SEXP W V U Z Y X PHI CONS ALLP (A1 . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALLP#4 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALLP#4 . NIL . VARIABLE .))) . NIL . (ALLP#4) . NIL . ALLP . NIL . 4 .)(|∀PHI1 U.SOMEP(PHI1,U)≡(∃X.MEMBER(X,U)∧PHI1(X))| . (AXIOM (TM& . |∀PHI1 U.SOMEP(PHI1,U)≡(∃X.MEMBER(X,U)∧PHI1(X))|)) . (LISTP SEXP W V U Z Y X PHI CONS SOMEP ALLP MEMBER PHI1) . NIL . (ALLP#5) . NIL . ALLP . NIL . 5 .)(|∀AV XV.XVεAV≡AV(XV)| . (DEFINE EPSILON (TM& . |∀AV XV.XVεAV≡AV(XV)|) NIL) . (URELEMENT ZV YV XV BV AV (EPSILON . (|(GROUND⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#6 . NIL . DEFINED .))) . NIL . (SETS#6 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 6 .)(|∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV| . (AXIOM (TM& . |∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV EPSILON) . NIL . (SETS#7) . NIL . SETS . NIL . 7 .)(NIL . (DECL INTERSECTION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∩) (BINDINGPOWER: 950) (PREFIXNAME: INTERSECTION)) . ((INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#8 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))| . (DEFINE INTERSECTION (TM& . |∀AV BV.AV∩BV=(λXV.AV(XV)∧BV(XV))|) NIL) . (URELEMENT ZV YV XV BV AV (INTERSECTION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SETS#9 . NIL . DEFINED .))) . NIL . (SETS#9 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 9 .)(NIL . (DECL UNION (TYPE: (TY& . |((@AV)⊗(@AV))→(@AV)|)) (INFIXNAME: ∪) (BINDINGPOWER: 950) (PREFIXNAME: UNION)) . ((UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#10 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 10 .)(|∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))| . (DEFINE UNION (TM& . |∀AV BV.AV∪BV=(λXV.AV(XV)∨BV(XV))|) NIL) . (URELEMENT ZV YV XV BV AV (UNION . (|((@AV)⊗(@AV))→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SETS#11 . NIL . DEFINED .))) . NIL . (SETS#11 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 11 .)(NIL . (DECL INCLUSION (TYPE: (TY& . |((@AV)⊗(@AV))→TRUTHVAL|)) (INFIXNAME: ⊂) (BINDINGPOWER: 920) (PREFIXNAME: INCLUSION)) . ((INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#12 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 12 .)(|∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))| . (DEFINE INCLUSION (TM& . |∀AV BV.AV⊂BV≡(∀XV.AV(XV)⊃BV(XV))|) NIL) . (URELEMENT ZV YV XV BV AV (INCLUSION . (|((@AV)⊗(@AV))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SETS#13 . NIL . DEFINED .))) . NIL . (SETS#13 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 13 .)(|EMPTYSET=(λXV.FALSE)| . (DEFAX EMPTYSET (TM& . |EMPTYSET=(λXV.FALSE)|)) . (URELEMENT ZV YV XV (EMPTYSET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#14 . NIL . DEFINED .))) . NIL . (SETS#14) . NIL . SETS . NIL . 14 .)(|∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))| . (DEFAX EMPTYP (TM& . |∀AV.EMPTYP(AV)=(∀XV.¬AV(XV))|)) . (URELEMENT ZV YV XV BV AV (EMPTYP . (|(GROUND→TRUTHVAL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#15 . NIL . DEFINED .))) . NIL . (SETS#15) . NIL . SETS . NIL . 15 .)(NIL . (DECL MKSET (TYPE: (TY& . |GROUND→(@AV)|))) . ((MKSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#16 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 16 .)(|∀X.MKSET(X)=(λYV.YV=X)| . (DEFINE MKSET (TM& . |∀X.MKSET(X)=(λYV.YV=X)|) NIL) . (SEXP Z Y X URELEMENT ZV YV XV AV (MKSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#17 . NIL . DEFINED .))) . NIL . (SETS#17 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 17 .)(NIL . (DECL MKLSET (TYPE: (TY& . |GROUND→(@AV)|))) . ((MKLSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#18 . NIL . VARIABLE .)) AV) . NIL . NIL . NIL . SETS . NIL . 18 .)(|∀U.MKLSET(U)=(λX.MEMBER(X,U))| . (DEFINE MKLSET (TM& . |∀U.MKLSET(U)=(λX.MEMBER(X,U))|) NIL) . (LISTP SEXP W V U Z Y X CONS MEMBER AV (MKLSET . (|GROUND→(@AV)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#19 . NIL . DEFINED .))) . NIL . (SETS#19 LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 SETS#3 SETS#4) . NIL . SETS . NIL . 19 .)(|∀U Y.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)| . (AXIOM (TM& . |∀U Y.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)|)) . (LISTP SEXP W V U Z Y X CONS MEMBER URELEMENT ZV YV XV BV AV INCLUSION MKSET MKLSET) . NIL . (SETFACTS#1) . NIL . SETFACTS . NIL . 1 .)(|∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV| . (AXIOM (TM& . |∀AV BV.AV⊂BV∧BV⊂AV⊃AV=BV|)) . (URELEMENT ZV YV XV BV AV INCLUSION) . NIL . (SETFACTS#2) . NIL . SETFACTS . NIL . 2 .)